From: Glenn Morris <rgm@gnu.org>
Date: Thu, 8 Dec 2016 00:43:36 +0000 (-0500)
Subject: Improve previous make-dist change
X-Git-Tag: archive/raspbian/1%29.2+1-2+rpi1^2~5^2~22^2~128
X-Git-Url: https://dgit.raspbian.org/%22http:/www.example.com/cgi/%22https:/www.github.com/%22bookmarks:///%22http:/www.example.com/cgi/%22https:/www.github.com/%22bookmarks:/?a=commitdiff_plain;h=953bf67;p=emacs.git

Improve previous make-dist change

* make-dist: Let make check the info files more thoroughly.
---

diff --git a/make-dist b/make-dist
index 6182b4931a1..31fa53a6f4d 100755
--- a/make-dist
+++ b/make-dist
@@ -281,6 +281,13 @@ if [ $check = yes ]; then
     echo "${bogosities}"
   fi
 
+  ## This exits with non-zero status if any .info files need
+  ## rebuilding.
+  if [ -e Makefile ]; then
+      echo "Checking to see if info files are up-to-date..."
+      make --question info || error=yes
+  fi
+
   [ $error = yes ] && exit 1
 fi